Nasledujúca kapitola obsahuje veci, ktoré neboli odprednášané doc.
Tomanom v roku, keď som dôkladne prerábal tieto poznámky. Evidentne
ale dané veci boli odprednášané rok predtým, odkiaľ sú aj nasledujúce
poznámky. Na začiatku by to chcelo snáď upozornenie, že dané poznámky
sú neoverené a z predchádzajúcich skúseností môžu byť chaotické a
neúplné (i keď základný obsah majú zachytený dobre).

Poprosil by som preto, ak máš poznámky k tejto časti, bolo by
najideálnejšie, ak by si vygeneroval/-a pripomienky k skriptám
a buď doručil/-a mne osobne alebo rovno prepísala zdrojové kódy
skrípt. Myslím, že Ti za to budú vďačné budúce generácie.

PPershing

\startFIXME

\section{Rozširovanie teórie}
\paragraph{Veta} Nech $A$ je formula teórie $T$ s jazykom $L$, nech všetky voľné
premenné formuly $A$ sú $x_1, x_2, \ldots x_n$, ďalej nech $L'$ je rozšírenie
$L$ pridaním nového predikátového symbolu $P$ a nech $T'$ vznikne z $T$ pridaním
axiomy $P(x_1, \ldots x_n) \iff A$ (označme ju *). 
\par Potom teória $T'$ s jazykom $L'$ je konzervatívne rozšírenie teórie $T$ s
jazykom $L$. Ďalej, pre každú formulu $B$ jazyka $L'$ existuje formula $B^*$ z
jazyka $L$, že platí $T \models  B \iff B^*$. 

\par Najprv budeme konštruovať $B^*$. Dôkaz: Nech $B$ je formula na jazyku $L'$,
nech $A'$ je variant  formuly $A$ (definujúcej predikát $P$), že žiadna
premennáz formuly $B$ nie je viazaná vo formule $A'$.

\par Nech $B^*$ vznikne z $B$ tak, že každú podformulu $P(a_1, \ldots a_n)$
nahradíme podformulou $A'(a_1, \ldots a_n)$ a podľa vety o variantoch nám platí,
že:
$$ T' \models P(a_1, \ldots, a_n) \iff A'(a_1, \ldots a_n)$$
$$ T' \models B \iff B^*$$.

\par Ukážeme, že $T'$ v jazyku $L'$ je konzervatívne rozšírenie teórie $T$ v
$L$ (teda pre ľubovoľnú formulu na pôvodnom jazyku, ktorá je dokázateľná v
teórii $L'$, je dokázateľná aj v pôvodnej teórii --  nevzniknú žiadne nové
teorémy). Nech $C$ je ľubovoľné formula na jazyku $L'$, ďalej nech platí $T'
\models C$. Nám stačí dokázať, že $T \models C^*$. Ak je potom formula $C$ na
jazyku $L$, potom $C^*$ je $C$.
\par Uvažujme $C_1, C_2, \ldots C_n$ je odvodenie formuly $C$ v teórii $T'$. Nám
stačí ukázať, že $C_i^*$ sú dokázateľné (odvoditeľné) v $T$.

Pri odvodení $C$ sa môže stať nasledovné:
\begin{enumerate}
	\item $C_i$ je axioma predikátovej logiky $L$, potom $C_i^*$ je axioma
	rovnakého druhu
	\item $C_i$ je axioma z $T$, potom $C_i^*$ je $C_i$ a teda je
	dokázateľná z $T$.
	\item Môže sa stať, že $C_i$ je axioma (x) $P(x_1,  \ldots, x_n) \iff
	A(x_1, \ldots, x_n)$. \par $C_i^*: A_i \iff A_i$, je dokázateľná pomocou
	vety o variantoch.
	\item Ak $C_i$ je odvodená z $C_j$ a $C_k$, použijeme pravidlo modus
	ponens. $C_i^*$ je odvodené z $C_j^*$ a $C_k^*$ tým istým pravidlom.
	\item $C_i$ je odvodené z $C_k$ pravidlom zovšeobecnenia ($k<i$). Potom
	$C_i^*$ je odvodené z $C_k^*$ pomocou toho istého pravidla.
\end{enumerate}



Ak máme teóriu $T$ a každá jej $A \in T$ je otvorená (každá premenná je voľná),
hovoríme o otvorenej teórii.

\par Majme danú teóriu $T$ s jazykom $L$. Máme k nej zostrojiť teóriu $T_H$
(henkinova teória) s jazykom $L(C)$, kde $C$ je zjednotenie konštánt všetkých
rádov. Dôležité pre nás budú konštanty $c_A, c_{\neg A}$.

\begin{itemize}
	\item $A_{c_{\neg A}} \implies (\forall x) A$ (*)
	\item $(\exists ) A \implies A(c_A)$ (**)
\end{itemize}

$$A \iff \neg \neg A$$
$$c_{\neg A} \iff \neg A(x)$$
$$\neg A(c_{\neg\neg A}) \implies (\forall x)\neg A$$
$$(\exists x) A \implies A(c_{\neg\neg A})$$
(Použili sme prenexnú operáciu).

\par Ak $c_{\neg A}$ je konštanta z axiomy s (*), tak hovoríme, že prislúcha
(patrí) formule A. Keď zoberieme formulu $A$.

$$(\forall x) A \implies A(t)$$ -- $t$ je term bez premenných v $L(C)$

$$A_{[c_{\neg A}]} \implies (\forall x) A \mbox{.......} c_{\neg A}$$

$\delta(T)$ množina na jazyku $L(C)$ prislchajúu konštante $C$ má ... axiomy
identity a ... a formúl z $T$.


\paragraph{Lema 1} Nech $A$ je formula na jazyku $L$ a ďalej, nech $A'$ je
uzavretá inštancia formuly $A$ na jazyku $L(C)$. Ak platí, že formula $A$ je
dokázateľná v pôvodnej teórii, potom $A'$ je tautologickým dôsledkom konečne
mnoho formúl z $\delta(T)$

\paragraph{Dôkaz} Nech $A_1, A_2, \ldots, A_n$ je dôkaz formuly $A$ v teórii
$T$. Indukciou podľa dĺžky dôkazu ukážeme, že ľubovoľná uzavretá formula v
jazyku $L(C)$ inštancia $A_j'$ formuly $A_j$ je tautologickým dôsledkom konečne
veľa formúl z $\delta(T)$.

\par Môžu nastať tieto prípady:
\begin{itemize}
	\item $A_j$ je axioma výrokovej logiky. Potom $A_j'$ je opäť tautológia.
	$A$ je tautologickým dôsledkom prázdnej množiny predpokladov.
	\item $A_j$ je axioma tvaru $(\forall x) B \implies B_x[t]$. Axioma
	špecifikácie. $A_j: (\forall x) B' \implies B_x'[t]]$ -- leží v
	$\delta T$. $t'$ je term bez premenných a je v $L(C)$. 
	\item $A_j$ je axioma $(\forall x) (C \implies D) \implies (C \implies
	(\forall x) D)$, $x$ nie je voľná v $C$.
	\par Uvažujme formulu $(\forall x) (C \implies D) \implies (C \implies
	(\forall x) D_x[c_{\neg D}])$. Táto formula patrí to $\delta(T)$, lebo
	je to inštancia axiomy špecifikácie.
	\par $ D_x[c_{\neg D}] \implies (\forall x) D$ -- opäť patrí do
	$\delta(T)$ (opäť (*))
	\par Tvrdíme, že formula $A_j$ je tautologický dôsledok horeuvedených 
	formúl. Budeme uvažovať takúto formulu:
	t -- $(A_1 \implies (B_1 \implies D_1)) \implies ((D_1 \implies C_1)
	\implies (A_1 \implies (B_1 \implies C_1)))$ Tvrdíme, že táto formula
	je teoréma.

	\par Dôkaz formuly: Za predpoklady si zoberiem formuly $A_1, (A_1
	\implies (B_1 \implies D_1))$, $B_1$, $(D_1 \implies C_1)$. Z týchto
	predpokladov dokážem odvodiť $C_1$.

	\par $A_1$ bude formula $(\forall x)(C \implies D)$, $B_1: C$, $C_1:
	(\forall x) D$, $D_1: D_x[c_{\neg D}]$

	\item $A_j$ je axioma z $T$, potom $A_j' \in \delta(T)$.
	\item $A_j$ je axioma identity alebo axioma rovnosti, potom $A_j'$ patrí
	do $\delta(T)$.

	\item $A_j$ dostaneme aplikáciou pravidla modu
	ponens z formúl $A_k$ a $A_l$, pričom $k, l < i$. $A_j'$ dostávame z
	$A_k'$ a $A_l'$ pomocou pravidla modus ponens.
	\item $A_j$ je odvodená z $A_k$ pravidlom zovšeobecnenia, pričom
	predpoklad je $k<j$. Teda $A_j: (\forall x) C$, teda $A_k: C$, x --
	premenná. Inštancia $A_j': (\forall x) C'$. Uvažujme inštanciu $A_k'$
	formuly $A_k$ v takomto tvare: $A_k:  C_k'[c_{\neg C'}]$. Podľa
	indukčného predpokladu je táto formula tautologickým dôsledkom konečne
	veľa formúl z $\delta (T)$. Uvažujme formulu $$C_x'[c_{\neg C'}]
	\implies (\forall x) C' \qquad \mbox{(***)}$$
	$A_j'$ je tautologickým dôsledkom formuly z $\delta(T)$. Dokázali sme
	formulu $A'$ tak, že sme nepoužili pravidlo zovšeobecnenia.
\end{itemize} 

\paragraph{Definícia} Hovoríme, že formula $A$ je \emph{kvázitautológia}, ak je
tautologickým dôsledkom inštancií axiom identity a rovnosti.

\paragraph{Veta (Hilbert-Ackermann)} Otvorená teória $T$ v jazyku $L$ (s
rovnosťou) je sporná práve vtedy, keď existuje (kvázi-)tautológia, ktorá je
disjunkciou negácií inštancií axiom z $T$.

\paragraph{Dôkaz} Najprv ľahšia implikácia: Predpokladajme, že sú splnené
podmienky vety, tak potom $T$ je sporná. Zoberme si nejakú formulu $A$. Berieme
$\neg A_1 \lor \neg A_2 \lor \ldots \lor \neg A_n$, kde $A_i$ sú inštancie axiom
z $T$. Pomocou de Morganovho zákona dostaneme $A_1 \land A_2 \land \ldots \land
A_n$. Ak platí $T \models A_i$, potom $T \models A_1 \land \ldots \land A_m$, a
teda $T$ je sporná, lebo je z nej dokázateľná ľubovoľná formula $B$, pretože
$\models A \implies (\neg A \implies B)$ a $T \models B$.

\par Naopak: Predpokladajme, že otvorená teória $T$ je sporná. $x \neq x$, $T
\models x \neq x$. Z toho vyplýva, že ak si zoberieme ľubovoľnú konštantu $r \in
C$, tak potom dostávame inštanciu formuly: $r \neq r$. To je uzavretá inštancia
teorémy vety z $T$, čiže podľa  Lemy 1 eistuje $A_1, A_2, \ldots A_k$  z $\delta
(T)$ také, že $r \neq r$ je tautologickým dôsledkom $A_1$ až $A_k$, teda z
predpokladov inštancií je dokázateľné $A_1, A_2, \ldots, A_k \models r \neq r$.
Platí $A_1 \implies A_2 \implies \ldots \implies A_k \implies r \neq r$ --
tautológia. $p \implies q \iff \neg p \lor q$. $\neg A_1 \lor \neg A_2 \lor
\ldots .. \lor \neg A_k \lor \neg (r=r)$ je tautológia. $A_i$ sú inštancie z
$\delta (T)$. Posledná formula je tautológia, ktorá je disjunkciou negácií
inštancií z $\delta (T)$.

\paragraph{Definícia} Postupnosť formúl $A_1, A_2, \ldots A_n$ nazveme
\emph{špeciálnou}, ak $\neg A_1\lor \neg A_2 \lor \ldots \lor \neg A_n$ je
tautológia. (Vieme) Ak $T$ je sporná teória, potom existuje špeciálna postupnosť
z $\delta (T)$



(pokračovanie)
\paragraph{Definícia} \emph{Stupeň konštanty} $c_{\neg A}$. $(\forall x) A$
uzavretá formula na jazyku $L(C)$. Hovoríme, že konštanta $c_{\neg A}$ spojená
axiomou $$A_{c_{\neg A}} \implies (\forall x) A$$ s formulou $(\forall x) A$ je
stupňa $n$, ak formula $(\forall x) A$ obsahuje $n$ výskytov kvantifikátorov
$\forall$ alebo $\exists$. 

\par Množina formúl $\delta_n(T)$ vznikne z $\delta(T)$ vynechaním všetkých
formúl stupňa $>n$ pre konštantu $c_{\neg A} \in C$. Treba si uvedomiť, že
stupeň konštanty $c_{\neg A}$ je vždy aspoň $1$. $\delta_0(T)$ -- uzavreté
inštancie, axiomy z množiny $T$ a axiom identity a rovnosti.

\par (Dokázali sme) Ak teória $T$ je sporná, existuje špeciálna postupnosť,
ktorá patrí do $\delta(T)$. Nech $n$ je najmenšie také $n$, že špeciálna
postupnosť z $\delta(T)$ je obsiahnutá v $\delta_n(T)$:

$n=0$. Musíme nájsť špeciálnu postupnosť prislúchajúcu do $T$.
Predpokladáme, že pre $n=0$ máme postupnosť $A_1, A_2, \ldots A_k$ --
špeciálna a patrí do $\delta_O(T)$. $c_A, c_{\neg A}$ nahradíme pomocou
premenných $A_1', A_2', \ldots A_k'$ (opäť špeciálna postupnosť). $A_1',
A_2', \ldots, A_n'$ sú všetky formuly, ktoré patria do $T$. $A_1', A_2',
\ldots A_k'$ budú inštancie axiom identity a rovnosti. $\neg A_1' \lor
\neg A_2' \lor \ldots \lor \neg A_n' \leftarrow A_{n+1} \leftarrow
\ldots \leftarrow A_k'$ -- kvázitautológia (vyplýva z toho, že táto
postupnosť je špeciálna). $A_1', A_2', \ldots A_n' \in T$.

\paragraph{Lema} Ak $n>0$ a existuje špeciálna postupnosť z $\delta_n(T)$, tak
potom existuje špeciálna postupnosť aj z $\delta_{n-1}(T)$.

\paragraph{Dôkaz} (pokračovanie dôkazu) Hilbert-Ackermanovej vety.
$\delta_0(T)$. Vieme vytvoriť postupnosť $B_1, B_2, \ldots, B_q \in T$.

\paragraph{Poznámka} Elementárna aritmetika je otvorená teória s konečným počtom
axiom. Hilbertova arigmetika, Presburgerova (??) aritmetika (aritmetika so
symbolmi $0, S, +$. Peanova aritmetika (1931).

\paragraph{Definícia} 
\begin{enumerate}
\item
Hovoríme, že formula $A$ je existenčná, ak $A$ je v
prenexnom tvare a všetky kvantifikátory v prefixe sú existenčné .
\item Hovoríme, že formula $A$ je univerzálna, ak $A$ je v prenexnom tvare a
všetky kvantifikátory sú univerzálne.

\end{enumerate}

\paragraph{Lema 3} Uzavretá existenčná formula $A$ je dokázateľná v predikátovej
logike (s rovnosťou) práve vtedy, keď istá disjunkcia otvoreného jadra formuly
$A$ je kvázitautológia.

\paragraph{Dôkaz} $A: (\exists x_1)(\exists x_2) \ldots (\exists x_n)B$
--formula v prenexnom tvare, $B$ je otvorené jadro. 

\begin{enumerate}
	\item Formulá $A$ je dokázateľná $\iff$ teória s jedinou špeciálnou
	axiomou $\neg A$ je sporná.
	\item Ak použijeme prenexné operácie, dostávame $\models \neg A \iff
	(\forall x_1)\ldots (\forall x_n) \neg B$. $\neg A \iff (\forall x_1)
	\ldots  (_n) \neg B$.

	\item Formula $A$ je dokázateľná $\iff$ keď teória $T$ s jedinou
	špeciálnou axiomou $\neg B$ je sporná. $\neg B$ je otvorená. Keď
	použijeme Hilbert-Ackermannovu vetu, dostávame $\neg B_1, \neg B_2
	\ldots, \neg B_m$ -- nad $\neg B$. Platí $\neg \neg B_1 \lor \neg \neg
	B_2 \lor \ldots \lor \neg \neg B_m$, čo je to isté ako $B_1 \lor B_2
	\lor \ldots \lor B_m$, čo je to isté, ako Hilbert-Ackermannova veta.
\end{enumerate}


\par Teóriu $T$ rozširujeme do $T_H$ s jazykom $L(C)$ a tú zase do $T_R$ s
$L(C)$. $A_x[C_{\neg A}] \implies (\forall x) A$ -- toto môžeme aj obrátiť:
$$(\forall x) A \implies A_x[c_{\neg A}]$$ -- vďaka axiome špecifikácie.
\par Ak teraz vezmeme formulu $B$ takú, že $A\iff B$, potom platí $B_x[c_{\neg
B}] \implies (\forall x) B$. 
$$
\begin{array}{lll}
T_H &\models& A_x[c_{\neg A}] \iff B_x[c_{\neg B}] \\
T_H &\models& A_x [c_{\neg A}] \iff (\forall x) A \\
T_H &\models& A \iff B \\
T_H &\models& (\forall x) A \iff (\forall x) B \\
T_H &\models& B_x[c_{\neg B}] \iff (\forall x) B \\
\end{array}
$$


$$(\forall x)(A\iff B) \implies c_{\neg A} = c_{\neg B}$$

\paragraph{Lema 4} Pre ľubovoľnú teóriu $T$ je $T_R$ konzervatívne rozšírenie.

\par Majme formulu $A$, ktorá je uzavretá a napísaná v prenexnom tvare.
Indukciou podľa počtu všeobecných kvantifikátorov budeme formulu transformovať
do tzv. Herbrandovho variantu. Ak formula $A$ má tvar:
$$ A: (\exists x_1) \ldots (\exists x_n) (\forall y) B, \qquad n \geq 0$$
$$ A^*: (\exists x_1) \ldots (\exists x_n) B_y[f(x\ldots x_n)]$$, $A^*$ je $A_H$

$A^{**}, L \cup \{ f,g,h, \ldots \}$.

\paragraph{Veta} (Herbrandova) Uzavretá formula v prenenom tvare je dokázateľnáv
predikátovej logike (s rovnosťou) práve vtedy, keď istá disjunkcia inštancií
otvoreného jadra je kvázitautológia.

\paragraph{Dôkaz} $A_H$ -- je existenčná formula. Je dokázateľná práve vtedy,
keď vezmeme do úvahy lemu 3 a platí formulácia našej vety. $L'$ .... ??? . Stačí
ukázať, že:
$$\models_L A \iff \models_{L'} A_H$$.
Implikácia zľava doprava je ľahšia -- vieme ukázať, že $\models_{L'} A \implies
\models_{L'} A^*$. Premennú $y$ sme nahradili funkciu $n$ premenných. Všimnime
si:

$$ \models_{L'} (\forall y) B \implies B_y[f(x_1\ldots x_n)]$$; axioma
špecifikácie. $(\exists x_1)(\exists x_2), \ldots (\exists x_n)$. Potom platí aj
$\models A \implies B$, $\models (\exists x) A \implies (\exists x) B$



\paragraph{Veta} (o zavedení funkčného symbolu) Nech formula $(\exists y) A$ je
dokázateľná v teórii $T$ s jazykom $L$. Nech $x_1, x_2, \ldots, x_n$ sú všetky
voľné premenné, ktoré sa vyskytujú vo formuli $(\exists y) A$. Nech $T'$ vznikne
z $T$ pridaním nového $n$-árneho funkčného symbolu $f$ a pridaním axiomy
$A_y[f(x_1, \ldots, x_n)]$. Potom $T'$ je konzervatívne rozšírenie teórie $T$.

\paragraph{Dôkaz} Nech $B$ je uzavretá formula teórie $T$ (s jazykom $L$).
Predpokladáme, že $B$ je teorémou (vetou teórie) $T'$. $T' \models B$. Máme
ukázať, že aj v $T \models B$. Predpokladajme, že formula $B$ má dôkaz v $T'$ a
že v tom dôkaze vystupujú $a_1, a_2, \ldots, a_n$ -- špeciálne axiomy teórie
$T$, prípadne axioma $(*)$. Na základe tohto predpokladu je v predikátovej
logike dokázateľná nasledovnaá formula.

$$(1) \models (\forall x_1) (\forall x_2) \ldots (\forall _n) a_y [f(x_1 \ldots
x_n)] \implies B_1 \implies B_2 \implies \ldots \implies B_n \implies B$$

$B_1, \ldots, B_n$ sú ...ny funkcií $A_1, A_2, \ldots, A_n$. 

$$ A_y[f(x_1, \ldots x_n)], A_1, \ldots, A_n \models B$$

Označme si $C$ -- prenexný tvar nasledovnej formuly:
$$A \implies B_1 \implies \ldots \implies B_n \implies B$$
Potom:

$$ (2) (\exists x_1) (\exists x_2) \ldots (\exists x_n) C_y[f(x_1, \ldots,
_n)]$$ je prenexný tvar $(1)$

Uvažujme $D: (\exists x_1) \ldots (\exists x_n) (\forall y) C$. Potom z tohto
vyplýva $D$ je formula jazyka $L$ a neobsahuje novo zavedený symbol $f$. Ak
konštruujeme herbrandovský variant tej podformuly ($D_H$) (meníme veľké
kvantifikátory) a na prvom kroku dostávame $D^*: (\exists x_1) \ldots (\exists
x_n) C_y [f(x_1, \ldots x_n)]$ -- prenexný tvar $(1)$. Z Herbrandovej vety
dostávame, že $D^*$ je dokázateľné, z tadiaľ $(D^*)_H$ je dokázateľné a z toho 
$(4) T \models D$

\par Prenexnými operáciami dostávame  $$(5) (\exists x_1) (\exists x_2) \ldots
(\exists x_n) (\forall y) (A \implies B_1 \implies \ldots \implies B_n \implies
B)$$

$$(6) T \models (\forall x_1 ) (\forall x_2) \ldots (\forall x_n) (\exists y)
A \implies B_1 \implies B_2 \implies \ldots \implies B_n \implies B$$

\par Každý z týchto predpokladov je dokázateľný v $T$, dostávame $T \models B$ a
teda $T'$ je konzervatívne rozšírenie $B$.

Mám formulu $A$, ktorá je uzavretá, idem priradiť skolemov tvar (skolemov
variant).
\begin{enumerate}
	\item Ak formula $A$ je univerzálna, potom $A_S$ je formula $A$
	\item Ak $A$ je tvaru $(\forall x_1) \ldots (\forall x_n) (\exists y) B,
	n\geq 0$, $f$ je funkčný symbol, kladieme $A_S: (\forall x_1) \ldots
	(\forall x_n) B_y[f(x_1,\ldots, x_n)]$, $(A')C ...$
\end{enumerate}

(1*) $A' \models A$ a ... $A_S \models A$
$ \models B_y[f(x_1, \ldots, x_n)] \implies (\exists y) B$ -- duálny tvar
axiomy špecifikácie. Teraz môžeme sformulovať Skolemovu vetu:

\paragraph{Veta} (Skolemova) V ľubovoľnej teórii $T$ môžeme zostrojiť otvorenú
teóriu $T'$, ktorá je konzervatívnym rozšírením teórie $T$.
\paragraph{Dôkaz} Mám teóriu $T$ s jazykom $L$. Zostrojím si teóriu $T_1$ s tým
istým jazykom a tá teória $T_1$ sú uzávery prenexných tvarov axiom z $T$. Z vety
o uzávere a vety o prenexnom tvare platí, že $T_1$ je konzervatívne rozšírenie
$T$ a naopak, $T$ je konzervatívne rozšírenie $T_1$. $T \equiv T_1$.

\par Teória $T_2$ vznikne z teórie $T_1$ tak, že ľubovoľnej formuli $A \in T_1$
zostrojíme skolemov variant $A_S$. V $T_2$ je konzervatívne rozšírenie $T_1$
podľa vety o zavedení funkčného symbolu. 

\par Ideme vytvárať teóriu $T_3$ -- vznikne z $T_2$ vynechaním všetkých axiom z
$T_1$. Podľa $(1^*)$ dostávame, že $T_2 \equiv T_3$.

\par Ďalej vytvárame teóriu $T_4$ -- pozostáva z otvorených jadier $T_3$, teda
$T_3 \equiv T_4$. Keď to zhrnieme, dostávame: $T \equiv T_1$, $T_2$ je
konzervatívne rozšírenie $T_1$. $T_2 \equiv T_3 \equiv T_4$, a z toho $T_4$ je
konzervatívne rozšírenie $T$.

\paragraph{Veta} (o zavedení funkcie pomocou definície) Majme teóriu $T$ s
jazykom $L$ a nech $x_1, \ldots, x_n, y$ sú navzájom rôzne premenné, ktoré sa
vyskytujú voľne vo formule $D$. Nech platí:
\begin{enumerate}
	\item $T\models  (\exists y) D$
	\item $T\models D \implies (D_y[y] \implies y = t)$
\end{enumerate}
Nech $L'$ vznikne z $L$ pridaním nového $n$-árneho funkčného symbolu $f$ a $T'$
z $T$ pridaním axiomy $$(3) y=f(x_1, \ldots x_n) \iff D$$ (definícia axiomy). Potom
$T'$ je konzervatívne rozšírenie $T$ a ku každej formule $A$ na jazyku $L'$
existuje formula $A^*$ na jazyku $L$ taká, že platí $$(4) T' \models A \iff A^*$$

\paragraph{Dôkaz} Najprv ukážeme, ako ku formuli $A$ priradiť formulu $A^*$, a
potom ukážeme, že $T'$ je konzervatívne rozšírenie $T$.

\par Zostrojíme $A^*$ z $A$ tak, aby platilo $(4)$. Formulu $A$ máme na jazyku
$L'$, problematický je symbol $f$ -- vyskytuje sa v atomických podformuliach.
Nech funkčný symbol $f$ sa vyskytuje vo formuli $A$ a nech je to ten
najvnútornejší výskyt. Je to nejaký $f(t_1, \ldots t_n)$, pričom $t_1, \ldots,
t_n$ už neobsahujú $f$. 

$$A: B_z[f(t_1, \ldots, t_b)]$$, a naše $z$ sa nevyskytuje vo formuli $A$, a ani
v definujúcej formuli $D$. Položme $A^*$  tvare:
$$(5) (\exists z) D'_{x_1, \ldots, x_n, y}[t_1, \ldots, t_n, z] \land B^*)$$,
pričom $D'$ je variant $D$, v ktorej nie je viazaná žiadna premenná, ktorá sa
vyskytuje vo formuli $A$. Z vety o variantoch a definujúcej axiomy $(3)$
dostávame, že na jazyku $L'$ je dokázané $ (6) \models_{L'} z = f(t_1, \ldots, t_n) \iff D'[t_1,
\ldots t_n, z]$. Z vety o ekvivalencii dostávame, že platí $$(7) T' \models
(\exists z) z = f(t_1, \ldots, t_n) \land B^*) \iff f^*$$. Z indukčného
predpokladu dostávame $$(8) T' \models B \iff B'$$

\par $(1) T' \models (\exists z) (z = f (t_1, \ldots, t_n) \land B) \iff A^*$ z
vedy o .... ($\models (\exists x) (x=t \land A) \iff A_x[t]$)
$$T' \models B_z[t_1, \ldots, t_n] \iff A^*$$, na ľavej strane je formula $A:
B_z[t_1, \ldots t_n]$.

\par Použijeme vetu o zavedení funkčného symbolu. Uvažujme $S$ -- teóriu z
jazyka $L'$, ktorá vznikne z $T$ pridaním axiomy:
$$(10) D_y[f(x_1, \ldots, x_n)]$$.

Ukážeme, že $T'$ a $S$ sú ekvivalentné a platí $T' \equiv S$. Potrebujeme
ukázať, že $(10)$ je teorémou $T'$ a $(3) y=f(x_1, \ldots, x_n) \iff D$ je
teorémou (vetou) $S$. V $T' \models f(x_1, \ldots x_n) = f(x_1, \ldots, _n)
\implies D_y[f(x_1, \ldots _n)]$, formula je inštancia axiomy $(3)$. Ak
použijeme inštanciu na axiomu identity $(3)$ $T' \models D_y[f(_1, \ldots,
x_n)]$. Potrebujeme ukázať, že $3$ je dokázateľná v $S$. Vyjdeme z tvaru $(11)
\models_{L'} y = f(x_1, \ldots x_n) \implies (D \iff D_y[f(x_1, \ldots, x_n)])$.

$$(12) \models_{L'} D_y[f'(x_1, \ldots, x_n)] \implies (y = f(x_1, \ldots _n
\implies D) $$

$$(13) S \models (y = f(x_1, \ldots, x_n) \implies D) \mbox{ z $(10)$}$$

$$(14) \models_{L'} D_y[f(x_1, \ldots, x_n) ] \implies (D \implies y = f(x_1,
\ldots x_n)] [T \models D \implies [D_y[t] \implies y = t) (2)$$


$$S \models D \implies y = f(x_1, \ldots x_n)$$
